$\forall$${\it es}$:ES, $i$:Id, $R$:(\{$e$:E$\mid$ loc($e$) $=$ $i$ \}$\rightarrow$Prop), $e$:E.
\\[0ex]($\forall$$e$:E. loc($e$) $=$ $i$ $\Rightarrow$ Dec($R$($e$)))
\\[0ex]$\Rightarrow$ loc($e$) $=$ $i$
\\[0ex]$\Rightarrow$ ($\exists$${\it e'}$:E. ${\it e'}$ $\leq$ $e$  \& $R$(${\it e'}$))
\\[0ex]$\Rightarrow$ ($\exists$${\it e'}$:E. ${\it e'}$ $\leq$ $e$  \& $R$(${\it e'}$) \& ($\forall$${\it e''}$:E. (${\it e'}$ $<$loc ${\it e''}$) $\Rightarrow$ ${\it e''}$ $\leq$ $e$  $\Rightarrow$ $\neg$$R$(${\it e''}$)))